Okay, let's restart.

So far, we've been looking at world description languages which we call logics.

We've looked at propositional logic and you've seen we call it PL0, basically predicate logic

with 0th order, which really you can translate into we have zero quantifiers.

And we've looked at first order logic, which you can think of we have one quantifier.

You can choose one and define the other one from it via strategically placed knots.

And there are logic above, second order logic you can imagine, third order logic up to any

order logic, we're not going to cover those.

And then there are even more expressive languages that allow you to do all kinds of wonderful

things with types, which is very computer sciencey and very nice, but we're not going

to cover them.

We've seen that it is good to have first order logic for being able to say things.

We've looked at Colonel West and his friends and the cats and so on.

And it was very good to be able to say things about individuals.

Unfortunately, there is a really, really hefty price to pay, namely we're losing decidability.

We've proven that in propositional logic we have decision procedures, namely we can implement

things like DPLL or Tableau or something like that and we know they will terminate in finite

time.

And give us an answer, is this satisfiable or is it not?

That is not something we have for first order logic anymore.

We're losing decidability.

We cannot guarantee that a resolution theorem prover will actually stop on a certain input

and give us an answer.

It might just run forever.

Or which is even worse, run so long that we don't know whether we have to just wait five

more minutes or there will never be an answer.

That is a hefty price to pay.

We have decidable.

Now you could say being decidable is a very good indication that the problems we can solve

with them are very boring.

And I would agree with you.

So intelligence is certainly not decidable.

But there's also some reasons you want decidability.

So you can ask yourselves where is the border to decidability?

Is it somewhere very near to propositional logic?

Or is it somewhere very near to first order logic?

And if it's the second, these logics should be good to know.

Some things where I can say almost the same things as in first order logic, have all the

convenience of first order logic without paying the price.

And we know that certain fragments of first order logic are decidable.

For instance, if we don't have any existentials, then we still have decidability.

And if we restrict ourselves to certain quantifier prefixes, like a universal quantifier and

then an existential quantifier and nothing else, then we still have decidability.

And there's a whole books and conferences of results of that nature.

So it is indeed the case that this is kind of where the border is.

So we do have logics that can almost arbitrarily go near the border.

And one such logic that has an enormous practical relevance is a logic called OWL2.

That's the Web Ontology Language.

That's kind of the web name.

There is also a name, that's the academic name, which basically says, oh, what do we